00100		ZERO←←274
00200		LOC ZERO
00300		PHASE	0
00400	
00500		DEFINE ABSO (N)		< (N)∧377 ↔ ((N)⊗-10)∧377 >
00600	
00700		DEFINE BRK		< 0 >
00800		DEFINE ORAIX (N)	< 1 ↔ (N)∧377 >
00900		DEFINE ORAZ (N)		< 5 ↔ (N)∧377 >
01000		DEFINE ASLZ (N)		< 6 ↔ (N)∧377 >
01100	
01200		DEFINE PHP		< 10 >
01300		DEFINE ORAI (N)		< 11 ↔ (N)∧377 >
01400		DEFINE ASLA		< 12 >
01500		DEFINE ORA (N)		< 15 ↔ (N)∧377 ↔ ((N)⊗-10)∧377 >
01600		DEFINE ASL (N)		< 16 ↔ (N)∧377 ↔ ((N)⊗-10)∧377 >
01700	
01800		DEFINE BPL (N)		< 20 ↔ ((N)-.-1) ∧ 377 >
01900		DEFINE ORAIY (N)	< 21 ↔ (N)∧377 >
02000		DEFINE ORAZX (N)	< 25 ↔ (N)∧377 >
02100		DEFINE ASLZX (N)	< 26 ↔ (N)∧377 >
02200	
02300		DEFINE CLC		< 30 >
02400		DEFINE ORAY (N)		< 31 ↔ (N)∧377 ↔ ((N)⊗-10)∧377 >
02500		DEFINE ORAX (N)		< 35 ↔ (N)∧377 ↔ ((N)⊗-10)∧377 >
02600		DEFINE ASLX (N)		< 36 ↔ (N)∧377 ↔ ((N)⊗-10)∧377 >
02700	
02800		DEFINE JSR (N)		< 40 ↔ (N)∧377 ↔ ((N)⊗-10)∧377 >
02900		DEFINE ANDIX (N)	< 41 ↔ (N)∧377 >
03000		DEFINE BITZ (N)		< 44 ↔ (N)∧377 >
03100		DEFINE ANDZ (N)		< 45 ↔ (N)∧377 >
03200		DEFINE ROLZ (N)		< 46 ↔ (N)∧377 >
     

00100		DEFINE PLP		< 50 >
00200		DEFINE ANDI (N)		< 51 ↔ (N)∧377 >
00300		DEFINE ROLA		< 52 >
00400		DEFINE BIT (N)		< 54 ↔ (N)∧377 ↔ ((N)⊗-10)∧377 >
00500		DEFINE AND (N)		< 55 ↔ (N)∧377 ↔ ((N)⊗-10)∧377 >
00600		DEFINE ROL (N)		< 56 ↔ (N)∧377 ↔ ((N)⊗-10)∧377 >
00700	
00800		DEFINE BMI (N)		< 60 ↔ ((N)-.-1) ∧ 377 >
00900		DEFINE ANDIY (N)	< 61 ↔ (N)∧377 >
01000		DEFINE ANDZX (N)	< 65 ↔ (N)∧377 >
01100		DEFINE ROLZX (N)	< 66 ↔ (N)∧377 >
01200	
01300		DEFINE SEC		< 70 >
01400		DEFINE ANDY (N)		< 71 ↔ (N)∧377 ↔ ((N)⊗-10)∧377 >
01500		DEFINE ANDX (N)		< 75 ↔ (N)∧377 ↔ ((N)⊗-10)∧377 >
01600		DEFINE ROLX (N)		< 76 ↔ (N)∧377 ↔ ((N)⊗-10)∧377 >
01700	
01800		DEFINE RTI		< 100 >
01900		DEFINE EORIX (N)	< 101 ↔ (N)∧377 >
02000		DEFINE EORZ (N)		< 105 ↔ (N)∧377 >
02100		DEFINE LSRZ (N)		< 106 ↔ (N)∧377 >
02200	
02300		DEFINE PHA		< 110 >
02400		DEFINE EORI (N)		< 111 ↔ (N)∧377 >
02500		DEFINE LSRA		< 112 >
02600		DEFINE JMP (N)		< 114 ↔ (N)∧377 ↔ ((N)⊗-10)∧377 >
02700		DEFINE EOR (N)		< 115 ↔ (N)∧377 ↔ ((N)⊗-10)∧377 >
02800		DEFINE LSR (N)		< 116 ↔ (N)∧377 ↔ ((N)⊗-10)∧377 >
     

00100		DEFINE BVC (N)		< 120 ↔ ((N)-.-1) ∧ 377 >
00200		DEFINE EORIY (N)	< 121 ↔ (N)∧377 >
00300		DEFINE EORZX (N)	< 125 ↔ (N)∧377 >
00400		DEFINE LSRZX (N)	< 126 ↔ (N)∧377 >
00500	
00600		DEFINE CLI		< 130 >
00700		DEFINE EORY (N)		< 131 ↔ (N)∧377 ↔ ((N)⊗-10)∧377 >
00800		DEFINE EORX (N)		< 135 ↔ (N)∧377 ↔ ((N)⊗-10)∧377 >
00900		DEFINE LSRX (N)		< 136 ↔ (N)∧377 ↔ ((N)⊗-10)∧377 >
01000	
01100		DEFINE RTS		< 140 >
01200		DEFINE ADCIX (N)	< 141 ↔ (N)∧377 >
01300		DEFINE ADCZ (N)		< 145 ↔ (N)∧377 >
01400		DEFINE RORZ (N)		< 146 ↔ (N)∧377 >
01500	
01600		DEFINE PLA		< 150 >
01700		DEFINE ADCI (N)		< 151 ↔ (N)∧377 >
01800		DEFINE RORA		< 152 >
01900		DEFINE JMPIN (N)	< 154 ↔ (N)∧377 ↔ ((N)⊗-10)∧377 >
02000		DEFINE ADC (N)		< 155 ↔ (N)∧377 ↔ ((N)⊗-10)∧377 >
02100		DEFINE ROR (N)		< 156 ↔ (N)∧377 ↔ ((N)⊗-10)∧377 >
02200	
02300		DEFINE BVS (N)		< 160 ↔ ((N)-.-1) ∧ 377 >
02400		DEFINE ADCIY (N)	< 161 ↔ (N)∧377 >
02500		DEFINE ADCZX (N)	< 165 ↔ (N)∧377 >
02600		DEFINE RORZX (N)	< 166 ↔ (N)∧377 >
     

00100		DEFINE SEI		< 170 >
00200		DEFINE ADCY (N)		< 171 ↔ (N)∧377 ↔ ((N)⊗-10)∧377 >
00300		DEFINE ADCX (N)		< 175 ↔ (N)∧377 ↔ ((N)⊗-10)∧377 >
00400		DEFINE RORX (N)		< 176 ↔ (N)∧377 ↔ ((N)⊗-10)∧377 >
00500	
00600		DEFINE STAIX (N)	< 201 ↔ (N)∧377 >
00700		DEFINE STYZ (N)		< 204 ↔ (N)∧377 >
00800		DEFINE STAZ (N)		< 205 ↔ (N)∧377 >
00900		DEFINE STXZ (N)		< 206 ↔ (N)∧377 >
01000	
01100		DEFINE DEY		< 210 >
01200		DEFINE TXA		< 212 >
01300		DEFINE STY (N)		< 214 ↔ (N)∧377 ↔ ((N)⊗-10)∧377 >
01400		DEFINE STA (N)		< 215 ↔ (N)∧377 ↔ ((N)⊗-10)∧377 >
01500		DEFINE STX (N)		< 216 ↔ (N)∧377 ↔ ((N)⊗-10)∧377 >
01600	
01700		DEFINE BCC (N)		< 220 ↔ ((N)-.-1) ∧ 377 >
01800		DEFINE STAIY (N)	< 221 ↔ (N)∧377 >
01900		DEFINE STYZX (N)	< 224 ↔ (N)∧377 >
02000		DEFINE STAZX (N)	< 225 ↔ (N)∧377 >
02100		DEFINE STXZY (N)	< 226 ↔ (N)∧377 >
02200	
02300		DEFINE TYA		< 230 >
02400		DEFINE STAY (N)		< 231 ↔ (N)∧377 ↔ ((N)⊗-10)∧377 >
02500		DEFINE TXS		< 232 >
02600		DEFINE STAX (N)		< 235 ↔ (N)∧377 ↔ ((N)⊗-10)∧377 >
02700	
02800		DEFINE LDYI (N)		< 240 ↔ (N)∧377 >
02900		DEFINE LDAIX (N)	< 241 ↔ (N)∧377 >
03000		DEFINE LDXI (N)		< 242 ↔ (N)∧377 >
03100		DEFINE LDYZ (N)		< 244 ↔ (N)∧377 >
03200		DEFINE LDAZ (N)		< 245 ↔ (N)∧377 >
03300		DEFINE LDXZ (N)		< 246 ↔ (N)∧377 >
     

00100		DEFINE TAY		< 250 >
00200		DEFINE LDAI (N)		< 251 ↔ (N)∧377 >
00300		DEFINE TAX		< 252 >
00400		DEFINE LDY (N)		< 254 ↔ (N)∧377 ↔ ((N)⊗-10)∧377 >
00500		DEFINE LDA (N)		< 255 ↔ (N)∧377 ↔ ((N)⊗-10)∧377 >
00600		DEFINE LDX (N)		< 256 ↔ (N)∧377 ↔ ((N)⊗-10)∧377 >
00700	
00800		DEFINE BCS (N)		< 260 ↔ ((N)-.-1) ∧ 377 >
00900		DEFINE LDAIY (N)	< 261 ↔ (N)∧377 >
01000		DEFINE LDYZX (N)	< 264 ↔ (N)∧377 >
01100		DEFINE LDAZX (N)	< 265 ↔ (N)∧377 >
01200		DEFINE LDXZY (N)	< 266 ↔ (N)∧377 >
01300	
01400		DEFINE CLV		< 270 >
01500		DEFINE LDAY (N)		< 271 ↔ (N)∧377 ↔ ((N)⊗-10)∧377 >
01600		DEFINE TSX		< 272 >
01700		DEFINE LDYX (N)		< 274 ↔ (N)∧377 ↔ ((N)⊗-10)∧377 >
01800		DEFINE LDAX (N)		< 275 ↔ (N)∧377 ↔ ((N)⊗-10)∧377 >
01900		DEFINE LDXY (N)		< 276 ↔ (N)∧377 ↔ ((N)⊗-10)∧377 >
02000	
02100		DEFINE CPYI (N)		< 300 ↔ (N)∧377 >
02200		DEFINE CMPIX (N)	< 301 ↔ (N)∧377 >
02300		DEFINE CPYZ (N)		< 304 ↔ (N)∧377 >
02400		DEFINE CMPZ (N)		< 305 ↔ (N)∧377 >
02500		DEFINE DECZ (N)		< 306 ↔ (N)∧377 >
02600	
02700		DEFINE INY		< 310 >
02800		DEFINE CMPI (N)		< 311 ↔ (N)∧377 >
02900		DEFINE DEX		< 312 >
03000		DEFINE CPY (N)		< 314 ↔ (N)∧377 ↔ ((N)⊗-10)∧377 >
03100		DEFINE CMP (N)		< 315 ↔ (N)∧377 ↔ ((N)⊗-10)∧377 >
03200		DEFINE DEC (N)		< 316 ↔ (N)∧377 ↔ ((N)⊗-10)∧377 >
     

00100		DEFINE BNE (N)		< 320 ↔ ((N)-.-1) ∧ 377 >
00200		DEFINE CMPIY (N)	< 321 ↔ (N)∧377 >
00300		DEFINE CMPZX (N)	< 325 ↔ (N)∧377 >
00400		DEFINE DECZX (N)	< 326 ↔ (N)∧377 >
00500	
00600		DEFINE CLD		< 330 >
00700		DEFINE CMPY (N)		< 331 ↔ (N)∧377 ↔ ((N)⊗-10)∧377 >
00800		DEFINE CMPX (N)		< 335 ↔ (N)∧377 ↔ ((N)⊗-10)∧377 >
00900		DEFINE DECX (N)		< 336 ↔ (N)∧377 ↔ ((N)⊗-10)∧377 >
01000	
01100		DEFINE CPXI (N)		< 340 ↔ (N)∧377 >
01200		DEFINE SBCIX (N)	< 341 ↔ (N)∧377 >
01300		DEFINE CPXZ (N)		< 344 ↔ (N)∧377 >
01400		DEFINE SBCZ (N)		< 345 ↔ (N)∧377 >
01500		DEFINE INCZ (N)		< 346 ↔ (N)∧377 >
01600	
01700		DEFINE INX		< 350 >
01800		DEFINE SBCI (N)		< 351 ↔ (N)∧377 >
01900		DEFINE NOP		< 352 >
02000		DEFINE CPX (N)		< 354 ↔ (N)∧377 ↔ ((N)⊗-10)∧377 >
02100		DEFINE SBC (N)		< 355 ↔ (N)∧377 ↔ ((N)⊗-10)∧377 >
02200		DEFINE INC (N)		< 356 ↔ (N)∧377 ↔ ((N)⊗-10)∧377 >
02300	
02400		DEFINE BEQ (N)		< 360 ↔ ((N)-.-1) ∧ 377 >
02500		DEFINE SBCIY (N)	< 361 ↔ (N)∧377 >
02600		DEFINE SBCZX (N)	< 365 ↔ (N)∧377 >
02700		DEFINE INCZX (N)	< 366 ↔ (N)∧377 >
02800	
02900		DEFINE SED		< 370 >
03000		DEFINE SBCY (N)		< 371 ↔ (N)∧377 ↔ ((N)⊗-10)∧377 >
03100		DEFINE SBCX (N)		< 375 ↔ (N)∧377 ↔ ((N)⊗-10)∧377 >
03200		DEFINE INCX (N)		< 376 ↔ (N)∧377 ↔ ((N)⊗-10)∧377 >